//generico utente
abstract sig Utente { }
//impiegato di TD
sig Impiegato extends Utente {
	pacchettiCreati: set PacchettoPredefinito,
    prodottiCreati: set Prodotto
 }
//cliente di TD
sig Cliente extends Utente {
    pacchettiCreati: set PacchettoPersonalizzato,
	prenotazioniEffettuate: set Prenotazione,
    invitiCreati: set Invito,
    email: Email
}
//chiave sul Cliente
sig Email {}

// prodotto generico
abstract sig Prodotto {
	luogo: Destinazione
}
// prodotti specifici
sig Volo extends Prodotto {
	dataAndata: Int,
	dataRitorno: Int
}
sig Hotel extends Prodotto {
	dataCheckin: Int,
    dataCheckout: Int
}
sig Escursione extends Prodotto {
	data: Int
}

// luogo a cui è riferito un pacchetto o un prodotto
sig Destinazione {}

// pacchetto astratto
abstract sig Pacchetto {
   dataInizio: Int,
   dataFine: Int,
   contiene: some Prodotto,
   viaggioPer: Destinazione
}
// pacchetto predefinito creato dall'impiegato
sig PacchettoPredefinito extends Pacchetto {
	scontoPercentuale: Int
}
// pacchetto personalizzato creato dal cliente
sig PacchettoPersonalizzato extends Pacchetto {}

// prenotazione
sig Prenotazione {
    riferitaA: Pacchetto
}

// invito
sig Invito {
	riferitoA: Prenotazione,
    emailRicevente: Email
}

// non ci sono Clienti diversi con la stessa email
fact noClientiStessaEmail {
	no c1, c2: Cliente | c1 != c2 and c1.email = c2.email
}

// per ogni invito deve esistere un Cliente che lo ha creato
fact invitoEsisteSeEsisteCreatore{
 all i: Invito | one c: Cliente | i in c.invitiCreati
}

// non esiste un invito tale che l'email del cliente che lo ha creato è uguale a quella del ricevente
fact noAutoInvito {
	no i: Invito, c: Cliente | i in c.invitiCreati and i.emailRicevente = c.email
}

// non esistono due inviti per la stessa prenotazione inviati alla stessa email (non esistono due inviti uguali)
fact {
   no i1, i2 : Invito | i1 != i2 and i1.emailRicevente = i2.emailRicevente and i1.riferitoA = i2.riferitoA
}

 // il creatore dell'invito è lo stesso di quello della prenotazione associata all'invito
fact stessoCreatoreInvitoPrenotazione {
	all c: Cliente, i: Invito | i in c.invitiCreati implies i.riferitoA in c.prenotazioniEffettuate
}

// per ogni prenotazione esiste un Cliente che l'ha effettuata
fact prenotazioneEsisteSeEsisteCreatore{
 all p: Prenotazione | one c: Cliente | p in c.prenotazioniEffettuate
}

// un cliente non effettua due prenotazioni diverse con lo stesso pacchetto 
fact noPrenotazioniStessoClienteStessoPacchetto {
  no c: Cliente, pr1,pr2: Prenotazione | 
       pr1 != pr2 and 
	   pr1 in c.prenotazioniEffettuate and pr2 in c.prenotazioniEffettuate and 
       pr1.riferitaA = pr2.riferitaA
}

// per ogni pacchetto esiste uno ed un solo Utente che l'ha creato
fact pacchettoEsisteSeEsisteCreatore{
	all p: PacchettoPredefinito | one i: Impiegato | p in i.pacchettiCreati 
	all p: PacchettoPersonalizzato | one c: Cliente | p in c.pacchettiCreati
}

// per ogni prodotto esiste uno ed un solo Impiegato che l'ha creato
fact prodottoEsisteSeEsisteCreatore{
	all p: Prodotto | one i: Impiegato | p in i.prodottiCreati 
}

// pacchetto personalizzato esiste solo se esiste una prenotazione riferita ad esso
// che è stata effettuata dallo stesso Cliente che lo ha creato
fact pacchettoPersonalizzatoEsisteSeEsistePrenotazioneAssociata {
	all c: Cliente, pp: PacchettoPersonalizzato | pp in c.pacchettiCreati implies
		one pr: Prenotazione | pr in c.prenotazioniEffettuate and  pr.riferitaA = pp
}

// un pacchetto può contenere solo prodotti che hanno la sua stessa destinazione
fact pacchettoContieneProdottiStessaDestinazione {
	all pa: Pacchetto,  pr: Prodotto | pr in pa.contiene implies pa.viaggioPer = pr.luogo
}

// un pacchetto è composto SOLO da prodotti di tipologie diverse
fact pacchettoContieneProdottiTipologieDiverse {
	all p1, p2: Hotel, pa: Pacchetto         |  (p1 != p2 and p1 in pa.contiene) implies p2 not in pa.contiene 
	all p1, p2: Volo, pa: Pacchetto           |  (p1 != p2 and  p1 in pa.contiene) implies p2 not in pa.contiene 
	all p1, p2: Escursione, pa: Pacchetto |  (p1 != p2 and  p1 in pa.contiene) implies p2 not in pa.contiene 
}

//non esistono pacchetti predefiniti con composizione identica
fact noPacchettiPredefinitiConUgualeComposizione {
	no p1,p2:PacchettoPredefinito | p1!=p2 and p1.contiene=p2.contiene
}

// cliente può prenotare pacchetto personalizzato solo se è il creatore o è stato invitato
fact prenotaPacchettoPersonalizzatoSoloSeCreatoreOInvitato {
	all c: Cliente, pr: Prenotazione, pp: PacchettoPersonalizzato | 
		 (pr in c.prenotazioniEffettuate and pr.riferitaA = pp) implies  // se il cliente ha prenotato il pacchetto
         (pp in c.pacchettiCreati or (one i: Invito | i.emailRicevente = c.email and i.riferitoA.riferitaA = pp)) // o lo ha creato o è stato invitato
}

// consistenza delle date nel pacchetto 
fact dateConsistentiPacchetto {
	// controllo hotel
	all p: Pacchetto, h: Hotel | h in p.contiene => (p.dataInizio = h.dataCheckin and p.dataFine=h.dataCheckout)
   // controllo voli
	all p: Pacchetto, v: Volo | v in p.contiene => (p.dataInizio = v.dataAndata and p.dataFine = v.dataRitorno)
   // controllo escursione
   all p: Pacchetto, e: Escursione | e in p.contiene => (e.data >= p.dataInizio and e.data <= p.dataFine)
}

/* START ANALISI DINAMICA */
pred aggiungiPrenotazione( c: Cliente, pr: Prenotazione ) { 
	pr not in c.prenotazioniEffettuate => 
		c.prenotazioniEffettuate = c.prenotazioniEffettuate + pr
}

pred nuovoPacchettoPersonalizzato(pp:PacchettoPredefinito,
		p':PacchettoPersonalizzato,pr: some Prodotto) {
	p'.contiene=pp.contiene+pr // ????? non capisco perchè. potremmo chiamarlo 'modificaPacchettoPredefinitoAggiungendoUnProdotto
}

pred clientePersonalizzaSuoViaggio( c , c': Cliente,ppr:PacchettoPredefinito,
		ppe':PacchettoPersonalizzato,pr: some Prodotto) {
	nuovoPacchettoPersonalizzato[ppr,ppe',pr]
	c'.pacchettiCreati=c.pacchettiCreati+ppe' //??? idem
}

pred clienteInvita ( e:Email,pr:Prenotazione,i':Invito) {
	i'.riferitoA=pr 
	i'.emailRicevente=e
}

pred clienteAccettaInvito(i:Invito , c , c':Cliente ) {
    i.emailRicevente = c.email => // se l'invito è per il cliente c
		aggiungiPrenotazione[c,i.riferitoA] // aggiungi la prenotazione a cui si riferisce
}

pred showAggiungiPrenotazione( c: Cliente, pr: Prenotazione) { 
	aggiungiPrenotazione[c, pr]
}

run showAggiungiPrenotazione for 3 but exactly 2 Cliente

